COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	revers.lsp[w82,jmc]	Axioms and proofs involving reverse
C00011 ENDMK
C⊗;
;;;revers.lsp[w82,jmc]	Axioms and proofs involving reverse
(wipe-out)
(get-proofs lispax)
(proof revers)
(context lispax#1:*)

(decl rev1 |ground⊗ground → ground| constant)
(axiom |∀u v. rev1(u,v) = if null u then v else rev1(cdr u, car u ~ v)|)
(lname definfo)

(∀e phi |λu.∀v.rev1(u,v) = reverse u * v| listinduction
|nil*([1#1#1]($definfo*nil*$definfo*nil*$definfo**simpinfo*nil))
*nil*([1#1#2](&definfo*nil**simpinfo*nil))
*nil| sortinfo)

(assume |∀v.rev1(u,v)=reverse u * v|)

(trw |rev1(u,x~v)| |-1| sortinfo)

(∀i v)

(ci -3 -1)

(∀i (x u))

(rw  4 |$9*nil|)